Muller Automaton
   HOME

TheInfoList



OR:

In
automata theory Automata theory is the study of abstract machines and automata, as well as the computational problems that can be solved using them. It is a theory in theoretical computer science. The word ''automata'' comes from the Greek word αὐτόματο ...
, a Muller automaton is a type of an
ω-automaton In automata theory, a branch of theoretical computer science, an ω-automaton (or stream automaton) is a variation of finite automata that runs on infinite, rather than finite, strings as input. Since ω-automata do not stop, they have a variety o ...
. The acceptance condition separates a Muller automaton from other ω-automata. The Muller automaton is defined using a Muller acceptance condition, i.e. the set of all states visited infinitely often must be an element of the acceptance set. Both deterministic and non-deterministic Muller automata recognize the
ω-regular language The ω-regular languages are a class of ω-languages that generalize the definition of regular languages to infinite words. Formal definition An ω-language ''L'' is ω-regular if it has the form * ''A''ω where ''A'' is a regular language n ...
s. They are named after
David E. Muller David Eugene Muller (November 2, 1924 – April 27, 2008) was an American mathematician and computer scientist. He was a professor of mathematics and computer science at the University of Illinois (1953–92), after which he became an emeritu ...
, an American
mathematician A mathematician is someone who uses an extensive knowledge of mathematics in their work, typically to solve mathematical problems. Mathematicians are concerned with numbers, data, quantity, structure, space, models, and change. History On ...
and
computer scientist A computer scientist is a person who is trained in the academic study of computer science. Computer scientists typically work on the theoretical side of computation, as opposed to the hardware side on which computer engineers mainly focus (al ...
, who invented them in 1963.


Formal definition

Formally, a deterministic Muller-automaton is a tuple ''A'' = (''Q'',Σ,δ,''q''0,F) that consists of the following information: * ''Q'' is a
finite set In mathematics, particularly set theory, a finite set is a set that has a finite number of elements. Informally, a finite set is a set which one could in principle count and finish counting. For example, :\ is a finite set with five elements. Th ...
. The elements of ''Q'' are called the ''states'' of ''A''. * Σ is a finite set called the ''alphabet'' of ''A''. * δ: ''Q'' × Σ → ''Q'' is a function, called the ''transition function'' of ''A''. * ''q''0 is an element of ''Q'', called the initial state. * F is a set of sets of states. Formally, F ⊆ P(''Q'') where P(''Q'') is
powerset In mathematics, the power set (or powerset) of a set is the set of all subsets of , including the empty set and itself. In axiomatic set theory (as developed, for example, in the ZFC axioms), the existence of the power set of any set is postu ...
of ''Q''. F defines the ''acceptance condition''. ''A'' accepts exactly those runs in which the set of infinitely often occurring states is an element of ''F'' In a non-deterministic Muller automaton, the transition function δ is replaced with a transition relation Δ that returns a set of states and the initial state ''q''0 is replaced by a set of initial states ''Q''0. Generally, 'Muller automaton' refers to a non-deterministic Muller automaton. For more comprehensive formalisation look at
ω-automaton In automata theory, a branch of theoretical computer science, an ω-automaton (or stream automaton) is a variation of finite automata that runs on infinite, rather than finite, strings as input. Since ω-automata do not stop, they have a variety o ...
.


Equivalence with other ω-automata

The Muller automata are equally
expressive Expressivity, expressiveness, and expressive power may refer to: *Expressivity (genetics), variations in a phenotype among individuals carrying a particular genotype *Expressive loa, a type of loanword in phono-semantic matching *Expressive power ...
as parity automata, Rabin automata, Streett automata, and non-deterministic
Büchi automata Buchi can mean: __NOTOC__ Items *Bachi, special Japanese drumsticks *Butsi, the Hispanised term for jin deui (pastry made from glutinous rice) in the Philippines *Büchi automaton, finite state automata extended to infinite inputs * Büchi arithmet ...
, to mention some, and strictly more expressive than the deterministic Büchi automata. The equivalence of the above automata and non-deterministic Muller automata can be shown very easily as the accepting conditions of these automata can be emulated using the acceptance condition of Muller automata and vice versa. McNaughton's theorem demonstrates the equivalence of non-deterministic Büchi automaton and deterministic Muller automaton. Thus, deterministic and non-deterministic Muller automata are equivalent in terms of the languages they can accept.


Transformation to non-deterministic Muller automata

Following is a list of automata constructions that each transforms a type of ω-automata to a non-deterministic Muller automaton. ;From
Büchi automata Buchi can mean: __NOTOC__ Items *Bachi, special Japanese drumsticks *Butsi, the Hispanised term for jin deui (pastry made from glutinous rice) in the Philippines *Büchi automaton, finite state automata extended to infinite inputs * Büchi arithmet ...
:If B is the set of final states in a Büchi automaton with the set of states Q, we can construct a Muller automaton with same set of states, transition function and initial state with the Muller accepting condition as F = . ;From Rabin automata/parity automata :Similarly, the Rabin conditions (E_j,F_j) can be emulated by constructing the acceptance set in the Muller automaton as all sets F \subseteq Q that satisfy F \cap E_j = \emptyset and F \cap F_j \neq \emptyset, for some ''j''. Note that this covers the case of parity automata too, as the parity acceptance condition can be expressed as a Rabin acceptance condition easily. ;From Streett automata :The Streett conditions (E_j,F_j) can be emulated by constructing the acceptance set in the Muller automaton as all sets F \subseteq Q that satisfy F \cap F_j = \emptyset \implies F \cap E_j = \emptyset, for all ''j''.


Transformation to deterministic Muller automata

;From Büchi automaton McNaughton's theorem provides a procedure to transform any non-deterministic Büchi automaton into a deterministic Muller automaton.


References

{{Reflist
Automata on Infinite Words
Slides for a tutorial by Paritosh K. Pandya. * Yde Venema (2008
Lectures on the Modal μ-calculus
th
2006 version
was presented at The 18th
European Summer School in Logic, Language and Information The European Summer School in Logic, Language and Information (ESSLLI) is an annual academic conference organized by the European Association for Logic, Language and Information. The focus of study is the "interface between linguistics, logic and ...
Finite automata Model checking